a:, n:. (a  n )  ((a rem n) = ((a - n) rem n)) 

latex

Up	int 2, int 2
Definitions	t  T, P  Q, x:A. B(x), P & Q, P  Q, P  Q, , , , False, A, A  B, i  j , S  T
Lemmas	nat wf, nat plus wf, ge wf, rem to div, nat plus inc int nzero, divide wfa, div rec case